ePMC - consensus disagree 6-2

Log
assertions-disabled
start-parsing
done-parsing
model-checking
analysing-property disagree
start-building-explorer
start-building-initial-states-explorer
done-building-initial-states-explorer
done-building-explorer
build-model-start
build-model-states-explored 10035 10035
build-model-states-explored 23843 13808
build-model-states-explored 41653 17810
build-model-states-explored 59006 17353
build-model-states-explored 81030 22024
build-model-states-explored 93893 12862
build-model-states-explored 121107 27215
build-model-states-explored 148538 27431
build-model-states-explored 177049 28511
build-model-states-explored 201353 24304
build-model-states-explored 209569 8216
build-model-states-explored 239711 30142
build-model-states-explored 268177 28466
build-model-states-explored 297468 29291
build-model-states-explored 326850 29382
build-model-states-explored 351003 24153
build-model-states-explored 375156 24153
build-model-states-explored 399166 24010
build-model-states-explored 423246 24080
build-model-states-explored 442401 19155
build-model-states-explored 442401 0
build-model-states-explored 451741 9340
build-model-states-explored 475689 23948
build-model-states-explored 499599 23910
build-model-states-explored 523221 23622
build-model-states-explored 546940 23719
build-model-states-explored 570858 23918
build-model-states-explored 594884 24026
build-model-states-explored 618748 23864
build-model-states-explored 642600 23851
build-model-states-explored 666463 23864
build-model-states-explored 690736 24273
build-model-states-explored 717421 26685
build-model-states-explored 744209 26788
build-model-states-explored 772349 28140
build-model-states-explored 801945 29596
build-model-states-explored 833191 31246
build-model-states-explored 864367 31175
build-model-states-explored 896388 32021
build-model-states-explored 927720 31332
build-model-states-explored 958546 30826
build-model-states-explored 989632 31086
build-model-states-explored 1000069 10437
build-model-states-explored 1000069 0
build-model-states-explored 1000069 0
build-model-states-explored 1000373 304
build-model-states-explored 1031431 31058
build-model-states-explored 1062071 30640
build-model-states-explored 1093240 31169
build-model-states-explored 1130529 37289
build-model-states-explored 1167909 37380
build-model-states-explored 1205363 37454
build-model-states-explored 1242900 37537
build-model-done 1258240 53
iterating
iterating-progress-unbounded 18 1.75 1
iterating-progress-unbounded 40 3.0 2
iterating-progress-unbounded 63 4.75 3
iterating-progress-unbounded 85 6.5 4
iterating-progress-unbounded 107 14.590909090909092 5
iterating-progress-unbounded 129 1.2150288352485883 6
iterating-progress-unbounded 151 0.5052937012201666 7
iterating-progress-unbounded 173 0.3013268362947567 8
iterating-progress-unbounded 195 0.21437352857744177 9
iterating-progress-unbounded 217 0.15536922860381366 10
iterating-progress-unbounded 239 0.12119075288949227 11
iterating-progress-unbounded 261 0.09806064777448294 12
iterating-progress-unbounded 283 0.08011560148703703 13
iterating-progress-unbounded 305 0.06779232040198518 14
iterating-progress-unbounded 327 0.05750157949204365 15
iterating-progress-unbounded 349 0.049697787079612546 16
iterating-progress-unbounded 371 0.043689665774182554 17
iterating-progress-unbounded 393 0.03811697814524766 18
iterating-progress-unbounded 415 0.033864840833208024 19
iterating-progress-unbounded 437 0.030098567874767158 20
iterating-progress-unbounded 459 0.02703300630526842 21
iterating-progress-unbounded 481 0.02450504315294635 22
iterating-progress-unbounded 502 0.022086403143243817 23
iterating-progress-unbounded 523 0.020156428162476935 24
iterating-progress-unbounded 545 0.018402126726835374 25
iterating-progress-unbounded 567 0.016749926229700576 26
iterating-progress-unbounded 589 0.015370252177829561 27
iterating-progress-unbounded 611 0.014185755517780067 28
iterating-progress-unbounded 633 0.012969714309576183 29
iterating-progress-unbounded 655 0.01198425532708601 30
iterating-progress-unbounded 677 0.011029228621121785 31
iterating-progress-unbounded 699 0.01022115273200422 32
iterating-progress-unbounded 721 0.00951372838534684 33
iterating-progress-unbounded 743 0.008773268014759415 34
iterating-progress-unbounded 765 0.008165725495084566 35
iterating-progress-unbounded 787 0.007566212333528109 36
iterating-progress-unbounded 809 0.007054399813603343 37
iterating-progress-unbounded 831 0.006600661653033399 38
iterating-progress-unbounded 853 0.006119689159133741 39
iterating-progress-unbounded 875 0.00572175416050957 40
iterating-progress-unbounded 897 0.005324377924722072 41
iterating-progress-unbounded 919 0.0049830622349352335 42
iterating-progress-unbounded 941 0.004677932410062941 43
iterating-progress-unbounded 963 0.004351737006288294 44
iterating-progress-unbounded 985 0.004080339732145868 45
iterating-progress-unbounded 1007 0.0038071448202515352 46
iterating-progress-unbounded 1029 0.0035715339393723577 47
iterating-progress-unbounded 1051 0.0033597158690009572 48
iterating-progress-unbounded 1073 0.003131976540969941 49
iterating-progress-unbounded 1096 0.002941790874023737 50
iterating-progress-unbounded 1118 0.0027439956408700805 51
iterating-progress-unbounded 1139 0.0025828606608533306 52
iterating-progress-unbounded 1161 0.0024326632588841574 53
iterating-progress-unbounded 1183 0.0022705555530915457 54
iterating-progress-unbounded 1205 0.0021348578205511314 55
iterating-progress-unbounded 1227 0.001997013158857994 56
iterating-progress-unbounded 1249 0.001877630850706257 57
iterating-progress-unbounded 1271 0.001769635018141166 58
iterating-progress-unbounded 1293 0.0016527800223177795 59
iterating-progress-unbounded 1315 0.001554823903327216 60
iterating-progress-unbounded 1337 0.0014550748052399678 61
iterating-progress-unbounded 1359 0.0013686130670268531 62
iterating-progress-unbounded 1381 0.0012902759319506484 63
iterating-progress-unbounded 1403 0.0012053758073549044 64
iterating-progress-unbounded 1425 0.0011341536525085539 65
iterating-progress-unbounded 1447 0.0010615133660594645 66
iterating-progress-unbounded 1469 9.985294583625417E-4 67
iterating-progress-unbounded 1491 9.414113934141789E-4 68
iterating-progress-unbounded 1513 8.794483047354955E-4 69
iterating-progress-unbounded 1535 8.274538758363926E-4 70
iterating-progress-unbounded 1557 7.743728837561905E-4 71
iterating-progress-unbounded 1579 7.283504358181293E-4 72
iterating-progress-unbounded 1601 6.865943902333646E-4 73
iterating-progress-unbounded 1623 6.412733806130266E-4 74
iterating-progress-unbounded 1645 6.032458468784886E-4 75
iterating-progress-unbounded 1667 5.644028452808952E-4 76
iterating-progress-unbounded 1689 5.307350642432265E-4 77
iterating-progress-unbounded 1711 5.00183438957782E-4 78
iterating-progress-unbounded 1733 4.6701717489384904E-4 79
iterating-progress-unbounded 1755 4.391960993548626E-4 80
iterating-progress-unbounded 1777 4.1077181774430265E-4 81
iterating-progress-unbounded 1799 3.861459390980575E-4 82
iterating-progress-unbounded 1821 3.6380051630441725E-4 83
iterating-progress-unbounded 1843 3.39543502431232E-4 84
iterating-progress-unbounded 1865 3.1920444161780517E-4 85
iterating-progress-unbounded 1887 2.984239203210754E-4 86
iterating-progress-unbounded 1909 2.8043042127855146E-4 87
iterating-progress-unbounded 1931 2.641064054028099E-4 88
iterating-progress-unbounded 1953 2.4638908561019603E-4 89
iterating-progress-unbounded 1975 2.3154103693366195E-4 90
iterating-progress-unbounded 1997 2.1637251740098802E-4 91
iterating-progress-unbounded 2019 2.0324643554009897E-4 92
iterating-progress-unbounded 2042 1.8959215748499286E-4 93
iterating-progress-unbounded 2064 1.7806144058952515E-4 94
iterating-progress-unbounded 2086 1.676050287424253E-4 95
iterating-progress-unbounded 2108 1.5626073974594692E-4 96
iterating-progress-unbounded 2130 1.4676119680538097E-4 97
iterating-progress-unbounded 2152 1.3705970397392844E-4 98
iterating-progress-unbounded 2174 1.2867209155956443E-4 99
iterating-progress-unbounded 2196 1.210686892021159E-4 100
iterating-progress-unbounded 2218 1.1282254900683817E-4 101
iterating-progress-unbounded 2240 1.0592137555386141E-4 102
iterating-progress-unbounded 2262 9.887551137111688E-5 103
iterating-progress-unbounded 2284 9.278776028831053E-5 104
iterating-progress-unbounded 2306 8.727130417924769E-5 105
iterating-progress-unbounded 2328 8.129076007724666E-5 106
iterating-progress-unbounded 2350 7.628855055400612E-5 107
iterating-progress-unbounded 2372 7.11830577886676E-5 108
iterating-progress-unbounded 2394 6.677456132736303E-5 109
iterating-progress-unbounded 2416 6.278132865624761E-5 110
iterating-progress-unbounded 2438 5.8453804487305146E-5 111
iterating-progress-unbounded 2460 5.483623787065113E-5 112
iterating-progress-unbounded 2482 5.11451675342733E-5 113
iterating-progress-unbounded 2504 4.79598981906356E-5 114
iterating-progress-unbounded 2526 4.507578121060512E-5 115
iterating-progress-unbounded 2548 4.195140465259568E-5 116
iterating-progress-unbounded 2570 3.9341010202041816E-5 117
iterating-progress-unbounded 2592 3.667843481130425E-5 118
iterating-progress-unbounded 2614 3.438202420495184E-5 119
iterating-progress-unbounded 2636 3.2303507203062216E-5 120
iterating-progress-unbounded 2658 3.0052670318917912E-5 121
iterating-progress-unbounded 2680 2.8173076071889506E-5 122
iterating-progress-unbounded 2702 2.6256514303124527E-5 123
iterating-progress-unbounded 2724 2.460440799030122E-5 124
iterating-progress-unbounded 2746 2.3109598185254594E-5 125
iterating-progress-unbounded 2768 2.14914340718509E-5 126
iterating-progress-unbounded 2790 2.0140816589339066E-5 127
iterating-progress-unbounded 2812 1.876405471740333E-5 128
iterating-progress-unbounded 2834 1.7577861167983337E-5 129
iterating-progress-unbounded 2856 1.650497156714374E-5 130
iterating-progress-unbounded 2878 1.534393690960678E-5 131
iterating-progress-unbounded 2900 1.43753082697432E-5 132
iterating-progress-unbounded 2922 1.3388216729769434E-5 133
iterating-progress-unbounded 2944 1.2538156823268555E-5 134
iterating-progress-unbounded 2966 1.1769542206569985E-5 135
iterating-progress-unbounded 2988 1.0938046209954878E-5 136
iterating-progress-unbounded 3010 1.024464115659815E-5 137
iterating-progress-unbounded 3032 9.538214203373869E-6 138
iterating-progress-unbounded 3054 8.930123934604476E-6 139
iterating-progress-unbounded 3076 8.380462859834746E-6 140
iterating-progress-unbounded 3098 7.786012125510998E-6 141
iterating-progress-unbounded 3120 7.29048280608813E-6 142
iterating-progress-unbounded 3141 6.852212169727311E-6 143
iterating-progress-unbounded 3162 6.37752286463983E-6 144
iterating-progress-unbounded 3184 5.969109103102432E-6 145
iterating-progress-unbounded 3206 5.60006231440089E-6 146
iterating-progress-unbounded 3228 5.201075963636617E-6 147
iterating-progress-unbounded 3250 4.868629909940494E-6 148
iterating-progress-unbounded 3272 4.530126537640716E-6 149
iterating-progress-unbounded 3294 4.238995067737282E-6 150
iterating-progress-unbounded 3316 3.975995417873112E-6 151
iterating-progress-unbounded 3338 3.6917340038112983E-6 152
iterating-progress-unbounded 3360 3.4549613904300334E-6 153
iterating-progress-unbounded 3382 3.2139296284236484E-6 154
iterating-progress-unbounded 3404 3.006702532826603E-6 155
iterating-progress-unbounded 3426 2.8195461010604393E-6 156
iterating-progress-unbounded 3448 2.617309041650565E-6 157
iterating-progress-unbounded 3470 2.4489120026367842E-6 158
iterating-progress-unbounded 3492 2.2775224639453596E-6 159
iterating-progress-unbounded 3514 2.1302190710437266E-6 160
iterating-progress-unbounded 3536 1.9972134635887416E-6 161
iterating-progress-unbounded 3558 1.8535236923218745E-6 162
iterating-progress-unbounded 3580 1.7339133522017863E-6 163
iterating-progress-unbounded 3602 1.6122019278435274E-6 164
iterating-progress-unbounded 3624 1.5076275629113685E-6 165
iterating-progress-unbounded 3646 1.4132241403772178E-6 166
iterating-progress-unbounded 3668 1.3112594567101083E-6 167
iterating-progress-unbounded 3690 1.2264058856259422E-6 168
iterating-progress-unbounded 3712 1.14007805322024E-6 169
iterating-progress-unbounded 3735 1.0641110371754665E-6 170
iterating-progress-unbounded 3757 9.89125402783536E-7 171
iterating-progress-unbounded 3778 9.267297737270496E-7 172
iterating-progress-unbounded 3800 8.666024620918766E-7 173
iterating-progress-unbounded 3822 8.05441324984864E-7 174
iterating-progress-unbounded 3844 7.529212613037291E-7 175
iterating-progress-unbounded 3866 7.055281216151731E-7 176
iterating-progress-unbounded 3888 6.543591539372641E-7 177
iterating-progress-unbounded 3910 6.117988922182939E-7 178
iterating-progress-unbounded 3932 5.685140637757417E-7 179
iterating-progress-unbounded 3954 5.313541741619145E-7 180
iterating-done 3974 180
model-checking-done 244
command-check-result-is 0.3636335471480052 disagree
Model:	consensus v.1 (MDP)
Parameter(s)	N = 6, K = 2
Property:	disagree (prob-reach)
Walltime:	245.76520991325378s
Return code:	0
Relative Error:	3.08059305525717e-05